/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ ↓H␈↓␈↓ εH␈↓ 91


␈↓ ↓H␈↓α␈↓ επChapter I

␈↓ ↓H␈↓α␈↓ ∧(PROVING LISP PROGRAMS CORRECT


␈↓ ↓H␈↓␈↓ α_The␈αtheory␈αof␈αcomputation␈α
may␈αbe␈αdivided␈αinto␈αtwo␈α
parts.␈α The␈αfirst␈αis␈αthe␈α
general␈αtheory
␈↓ ↓H␈↓of␈α
computability␈α
including␈α
topics␈α
like␈α
universal␈α
functions,␈α
the␈α
existence␈α
of␈αuncomputable␈α
functions,
␈↓ ↓H␈↓call-by-name␈α↔and␈α↔call-by-value,␈α↔and␈α↔the␈α_relation␈α↔of␈α↔conditional␈α↔form␈α↔recursion␈α_to␈α↔other
␈↓ ↓H␈↓formalisms␈α
for␈α
describing␈α
computable␈α∞functions.␈α
 The␈α
second␈α
part,␈α∞which␈α
we␈α
will␈α
discuss␈α∞in␈α
this
␈↓ ↓H␈↓chapter emphasizes techniques for proving particular facts about particular computable functions.

␈↓ ↓H␈↓␈↓ α_In␈α∩this␈α⊃chapter␈α∩we␈α⊃will␈α∩introduce␈α∩techniques␈α⊃for␈α∩proving␈α⊃LISP␈α∩functions␈α∩correct.␈α⊃ The
␈↓ ↓H␈↓techniques␈αwill␈αbe␈αlimited␈αto␈αwhat␈αwe␈αmay␈αcall␈α␈↓↓clean␈↓␈αLISP␈αfunctions.␈α In␈αparticular,␈αthere␈αmust␈αbe
␈↓ ↓H␈↓no␈α∂side␈α∂effects,␈α∂because␈α∂our␈α∂methods␈α∂depend␈α∂on␈α∂the␈α∂ability␈α∂to␈α∂replace␈α∂subexpressions␈α∂by␈α∂equal
␈↓ ↓H␈↓expressions.␈α Moreover,␈α
equality␈αmeans␈α
equality␈αof␈α
S-expressions␈αand␈α
not␈αequality␈α
of␈αlist␈α
structure.
␈↓ ↓H␈↓Thus the equal sign = corresponds to the Lisp function EQUAL, and EQ isn't used.

␈↓ ↓H␈↓␈↓ α_The␈α necessary␈αbasic␈αfacts␈αcan␈αbe␈αdivided␈αinto␈αseveral␈αcategories:␈αfirst␈αorder␈αlogic␈αincluding
␈↓ ↓H␈↓conditional␈α↔forms␈α_and␈α↔first␈α↔order␈α_lambda-expressions,␈α↔algebraic␈α↔facts␈α_about␈α↔lists␈α_and␈α↔S-
␈↓ ↓H␈↓expressions,␈αfacts␈αabout␈αthe␈αinductive␈αstructure␈αof␈αlists␈αand␈αS-expressions,␈αand␈αgeneral␈αfacts␈αabout
␈↓ ↓H␈↓functions defined by recursion.



␈↓ ↓H␈↓1.  ␈↓αFirst order logic with conditional forms and lambda-expressions.␈↓


␈↓ ↓H␈↓␈↓ α_The␈α∂logic␈α∂we␈α∂shall␈α∂use␈α∂is␈α∂called␈α∂first␈α∂order␈α∂logic␈α∂with␈α∂equality,␈α∂but␈α∂we␈α∂will␈α∂extend␈α⊂it␈α∂by
␈↓ ↓H␈↓allowing␈αconditional␈αforms␈αto␈αbe␈αterms␈αand␈αlambda-expressions␈αto␈αbe␈αfunction␈αexpressions.␈α From
␈↓ ↓H␈↓the␈α∞mathematical␈α∞point␈α∂of␈α∞view,␈α∞these␈α∂extensions␈α∞are␈α∞inessential,␈α∞because,␈α∂as␈α∞we␈α∞shall␈α∂see,␈α∞every
␈↓ ↓H␈↓sentence␈αthat␈α
includes␈αconditional␈αforms␈α
or␈αfirst␈αorder␈α
lambdas␈αcan␈αreadily␈α
be␈αtransformed␈αinto␈α
an
␈↓ ↓H␈↓equivalent␈α
sentence␈α
without␈α
them.␈α
 However,␈αthe␈α
extensions␈α
are␈α
practically␈α
important,␈αbecause␈α
they
␈↓ ↓H␈↓permit us to use recursive definitions directly as formulas of the logic.

␈↓ ↓H␈↓␈↓ α_Formulas␈α∂of␈α∞the␈α∂logic␈α∞are␈α∂built␈α∂from␈α∞constants,␈α∂variables␈α∞predicate␈α∂symbols,␈α∂and␈α∞function
␈↓ ↓H␈↓symbols␈α⊂using␈α⊂function␈α∂application,␈α⊂conditional␈α⊂forms,␈α∂boolean␈α⊂forms,␈α⊂lambda␈α⊂expressions,␈α∂and
␈↓ ↓H␈↓quantifiers.

␈↓ ↓H␈↓␈↓αConstants␈↓:␈α∞We␈α
will␈α∞use␈α∞S-expresssions␈α
as␈α∞constants␈α
standing␈α∞for␈α∞themselves␈α
and␈α∞also␈α∞lower␈α
case
␈↓ ↓H␈↓letters␈α∩from␈α∩the␈α∩first␈α∩part␈α∩of␈α∩the␈α∪alphabet␈α∩to␈α∩represent␈α∩constants␈α∩in␈α∩other␈α∩domains␈α∪than␈α∩S-
␈↓ ↓H␈↓expressions.

␈↓ ↓H␈↓␈↓αVariables␈↓:␈αWe␈αwill␈αuse␈αthe␈αletters␈α␈↓↓u␈↓␈αthru␈α␈↓↓z␈↓␈αwith␈αor␈αwithout␈αsubscripts␈αas␈αvariables.␈α The␈αvariables
␈↓ ↓H␈↓␈↓↓u␈↓ and ␈↓↓v␈↓ will usually stand for lists while ␈↓↓x␈↓ thru ␈↓↓z␈↓ will stand for S-expressions.

␈↓ ↓H␈↓␈↓αFunction␈αsymbols␈↓:␈αThe␈α
letters␈α␈↓↓f␈↓,␈α␈↓↓g␈↓␈α
and␈α␈↓↓h␈↓␈αwith␈α
or␈αwithout␈αsubscripts␈α
are␈αused␈αas␈αfunction␈α
symbols.
␈↓ ↓H␈↓The␈α⊂LISP␈α⊃function␈α⊂symbols␈α⊃␈↓αa␈↓,␈α⊂␈↓αd␈↓␈α⊃and␈α⊂.␈α⊃(as␈α⊂an␈α⊃infix)␈α⊂are␈α⊃also␈α⊂used␈α⊃as␈α⊂function␈α⊃symbols.␈α⊂ We
␈↓ ↓H␈↓suppose␈α
that␈αeach␈α
function␈αsymbol␈α
takes␈αthe␈α
same␈αdefinite␈α
number␈αof␈α
arguments␈αevery␈α
time␈α
it␈αis
␈↓ ↓H␈↓used.␈α We␈αwill␈αoften␈αuse␈αone␈αargument␈α
functions␈αsymbols␈αas␈αprefixes,␈αi.e.␈α without␈αbrackets,␈αjust␈α
as
␈↓ ↓H␈↓␈↓αa␈↓ and ␈↓αd␈↓ have been used up to now.
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 92


␈↓ ↓H␈↓␈↓αPredicate␈α∩symbols␈↓:␈α∩The␈α⊃letters␈α∩␈↓↓p␈↓,␈α∩␈↓↓q␈↓␈α⊃and␈α∩␈↓↓r␈↓␈α∩with␈α⊃or␈α∩without␈α∩subscripts␈α⊃are␈α∩used␈α∩as␈α⊃predicate
␈↓ ↓H␈↓symbols.␈α∂ We␈α∂will␈α∂also␈α∂use␈α∞the␈α∂LISP␈α∂predicate␈α∂symbol␈α∂␈↓αat␈↓␈α∞as␈α∂a␈α∂constant␈α∂predicate␈α∂symbol.␈α∞ The
␈↓ ↓H␈↓equality␈αsymbol␈α=␈α
is␈αalso␈αused␈α
as␈αan␈αinfix.␈α We␈α
suppose␈αthat␈αeach␈α
predicate␈αsymbol␈αtakes␈αthe␈α
same
␈↓ ↓H␈↓definite␈α∞number␈α
of␈α∞arguments␈α
each␈α∞time␈α
it␈α∞is␈α
used.␈α∞ Infix␈α
and␈α∞prefix␈α
notation␈α∞will␈α
also␈α∞be␈α
used
␈↓ ↓H␈↓where this is customary.

␈↓ ↓H␈↓␈↓ α_Next␈αwe␈αdefine␈αterms,␈αsentences,␈αfunction␈αexpressions␈αand␈αpredicate␈αexpressions␈αinductively.
␈↓ ↓H␈↓A␈αterm␈αis␈αan␈αexpression␈αwhose␈αvalue␈αwill␈αbe␈αan␈αobject␈αlike␈αan␈αS-expression␈αor␈αa␈αnumber␈αwhile␈αa
␈↓ ↓H␈↓sentence␈αhas␈αvalue␈αT␈αor␈αF.␈α Terms␈αare␈αused␈αin␈αmaking␈αsentences,␈αand␈αsentences␈αoccur␈αin␈αterms␈αso
␈↓ ↓H␈↓that␈α∪the␈α∪definitions␈α∪are␈α∪␈↓↓mutually␈α∪recursive␈↓␈α∪where␈α∪this␈α∪use␈α∪of␈α∪the␈α∪word␈α∪␈↓↓recursive␈↓␈α∪should␈α∪be
␈↓ ↓H␈↓distinguished␈α⊂from␈α⊂its␈α∂use␈α⊂in␈α⊂recursive␈α∂definitions␈α⊂of␈α⊂functions.␈α∂ Function␈α⊂expressions␈α⊂are␈α∂also
␈↓ ↓H␈↓involved in the mutual recursion.

␈↓ ↓H␈↓␈↓αTerms␈↓:␈α⊂Constants␈α⊃are␈α⊂terms,␈α⊃and␈α⊂variables␈α⊃are␈α⊂terms.␈α⊃ If␈α⊂␈↓↓f␈↓␈α⊃is␈α⊂a␈α⊃function␈α⊂expression␈α⊃taking␈α⊂␈↓↓n␈↓
␈↓ ↓H␈↓arguments,␈α
and␈α
␈↓↓t␈↓β1␈↓↓, ... ,t␈↓βn␈↓↓␈↓␈α
are␈α
terms,␈α
then␈α
␈↓↓f[t␈↓β1␈↓↓, ... ,t␈↓βn␈↓↓]␈↓␈α
is␈α
a␈α
term.␈α
 If␈α
␈↓↓p␈↓␈α
is␈α
a␈α
sentence␈α
and␈α
␈↓↓t␈↓β1␈↓↓␈↓␈αand␈α
␈↓↓t␈↓β2␈↓
␈↓ ↓H␈↓are␈α
terms,␈α∞then␈α
␈↓αif␈↓␈↓↓ p ␈↓αthen␈↓↓ t␈↓β1␈↓↓ ␈↓αelse␈↓↓ t␈↓β2␈↓␈α
is␈α∞a␈α
term.␈α
 We␈α∞soften␈α
the␈α
notation␈α∞by␈α
allowing␈α∞infix␈α
symbols
␈↓ ↓H␈↓where this is customary.

␈↓ ↓H␈↓␈↓αSentences␈↓:␈α⊂If␈α⊃␈↓↓p␈↓␈α⊂is␈α⊂a␈α⊃predicate␈α⊂expression␈α⊂taking␈α⊃␈↓↓n␈↓␈α⊂arguments␈α⊂and␈α⊃␈↓↓t␈↓β1␈↓↓, ... ,t␈↓βn␈↓↓␈↓␈α⊂are␈α⊃terms,␈α⊂then
␈↓ ↓H␈↓␈↓↓p[t␈↓β1␈↓↓, ... ,t␈↓βn␈↓↓]␈↓␈α∪is␈α∪a␈α∀sentence.␈α∪ Equality␈α∪is␈α∀also␈α∪used␈α∪as␈α∪an␈α∀infixed␈α∪predicate␈α∪symbol␈α∀to␈α∪form
␈↓ ↓H␈↓sentences,␈αi.e.␈α␈↓↓t␈↓β1␈↓↓ = t␈↓β2␈↓␈αis␈αa␈αsentence.␈α
 If␈α␈↓↓p␈↓␈αis␈αa␈αsentence,␈αthen␈α␈↓↓¬p␈↓␈α
is␈αalso␈αa␈αsentence.␈α If␈α␈↓↓p␈↓␈αand␈α
␈↓↓q␈↓␈αare
␈↓ ↓H␈↓sentences,␈α∃then␈α∃␈↓↓p∧q␈↓,␈α∃␈↓↓p∨q␈↓,␈α∃␈↓↓p⊃q␈↓,␈α∃and␈α∃␈↓↓p≡q␈↓␈α∃are␈α∀sentences.␈α∃ If␈α∃␈↓↓p␈↓,␈α∃␈↓↓q␈↓␈α∃and␈α∃␈↓↓r␈↓␈α∃are␈α∃sentences,␈α∀then
␈↓ ↓H␈↓␈↓αif␈↓␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ r␈↓␈α
is␈α
a␈α
sentence.␈α
 If␈α
␈↓↓x␈↓β1␈↓↓, ..., x␈↓βn␈↓↓␈↓␈α
are␈αvariables,␈α
and␈α
␈↓↓p␈↓␈α
is␈α
a␈α
term,␈α
then␈α␈↓↓∀x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:t␈↓␈α
and
␈↓ ↓H␈↓␈↓↓∀x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:t␈↓ are sentences.

␈↓ ↓H␈↓␈↓αFunction␈α
expressions␈↓:␈α∞A␈α
function␈α
symbol␈α∞is␈α
a␈α
function␈α∞expression.␈α
 If␈α
␈↓↓x␈↓β1␈↓↓, ... ,x␈↓βn␈↓↓␈↓␈α∞are␈α
variables
␈↓ ↓H␈↓and ␈↓↓t␈↓ is a term, then ␈↓↓[λx␈↓β1␈↓↓, ... ,x␈↓βn␈↓↓:t]␈↓ is a function expression.

␈↓ ↓H␈↓␈↓αPredicate␈αexpressions␈↓:␈αA␈αpredicate␈αsymbol␈αis␈αa␈αpredicate␈αexpression.␈α If␈α␈↓↓x␈↓β1␈↓↓, ... ,x␈↓βn␈↓↓␈↓␈αare␈αvariables
␈↓ ↓H␈↓and ␈↓↓p␈↓ is a sentence, then ␈↓↓[λx␈↓β1␈↓↓, ... ,x␈↓βn␈↓↓:p]␈↓ is a predicate expression.

␈↓ ↓H␈↓␈↓ α_An␈αoccurrence␈αof␈αa␈αvariable␈α␈↓↓x␈↓␈αis␈αcalled␈αbound␈αif␈αit␈αis␈αin␈αan␈αexpression␈αof␈αone␈αof␈αthe␈αforms
␈↓ ↓H␈↓␈↓↓[λx␈↓β1␈↓↓ ... x␈↓βn␈↓↓:t]␈↓,␈α
␈↓↓[λx␈↓β1␈↓↓ ... x␈↓βn␈↓↓:p]␈↓,␈α
␈↓↓[∀x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:p]␈↓␈αor␈α
␈↓↓[∃x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:p]␈↓␈α
where␈α␈↓↓x␈↓␈α
is␈α
one␈αof␈α
the␈α
numbered␈α␈↓↓x␈↓'s.␈α
 If
␈↓ ↓H␈↓not bound an occurrence is called free.

␈↓ ↓H␈↓␈↓ α_The␈α
␈↓↓semantics␈↓␈αof␈α
first␈αorder␈α
logic␈αconsists␈α
of␈α
the␈αrules␈α
that␈αenable␈α
us␈αto␈α
determine␈α
when␈αa
␈↓ ↓H␈↓sentence␈αis␈αtrue␈αand␈αwhen␈αit␈αis␈αfalse.␈α However,␈αthe␈αtruth␈αor␈αfalsity␈αof␈αa␈αsentence␈αis␈αrelative␈αto␈αthe
␈↓ ↓H␈↓interpretation␈αassigned␈αto␈αthe␈αconstants,␈αthe␈αfunction␈αand␈αpredicate␈αsymbols␈αand␈αthe␈αfree␈α
variables
␈↓ ↓H␈↓of the formula.  We proceed as follows:

␈↓ ↓H␈↓␈↓ α_We␈α
begin␈αby␈α
choosing␈α
a␈αdomain.␈α
 In␈αmost␈α
cases␈α
we␈αshall␈α
consider␈αthe␈α
domain␈α
will␈αinclude
␈↓ ↓H␈↓the␈αS-expressions␈αand␈αany␈αS-expression␈αconstants␈αappearing␈αin␈αthe␈αformula␈αstand␈αfor␈αthemselves.
␈↓ ↓H␈↓We␈α
will␈α
allow␈α
for␈α
the␈α
possibility␈α
that␈α
other␈α
objects␈α
than␈α
S-expressions␈α
exist,␈α
and␈α
some␈αconstants
␈↓ ↓H␈↓may␈α
designate␈αthem.␈α
 Each␈αfunction␈α
or␈αpredicate␈α
symbol␈αis␈α
assigned␈αa␈α
function␈αor␈α
predicate␈αon␈α
the
␈↓ ↓H␈↓domain.␈α∃ We␈α∃will␈α⊗normally␈α∃assign␈α∃to␈α⊗the␈α∃basic␈α∃LISP␈α⊗function␈α∃and␈α∃predicate␈α⊗symbols␈α∃the
␈↓ ↓H␈↓corresponding␈αbasic␈αLISP␈α
functions␈αand␈αpredicates.␈α
 Each␈αvariable␈αappearing␈α
free␈αin␈αa␈αsentence␈α
is
␈↓ ↓H␈↓also␈α
assigned␈α∞an␈α
element␈α∞of␈α
the␈α∞domain.␈α
 All␈α∞these␈α
assignments␈α∞constitute␈α
an␈α∞interpretation,␈α
and
␈↓ ↓H␈↓the truth of a sentence is relative to the interpretation.
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 93


␈↓ ↓H␈↓␈↓ α_The␈α⊂truth␈α∂of␈α⊂a␈α∂sentence␈α⊂is␈α⊂determined␈α∂from␈α⊂the␈α∂values␈α⊂of␈α∂its␈α⊂constituents␈α⊂by␈α∂evaluating
␈↓ ↓H␈↓successively␈α∞larger␈α∞subexpressions.␈α
 The␈α∞rules␈α∞for␈α
handling␈α∞functions␈α∞and␈α∞predicates,␈α
conditional
␈↓ ↓H␈↓expressions,␈αequality,␈αand␈αBoolean␈αexpressions␈αare␈αexactly␈αthe␈αsame␈αas␈αthose␈αwe␈αhave␈αused␈αin␈αthe
␈↓ ↓H␈↓previous chapters.  We need only explain quantifiers:

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:e␈↓␈αis␈αassigned␈αtrue␈αif␈αand␈αonly␈αif␈α␈↓↓e␈↓␈αis␈αassigned␈αtrue␈αfor␈αall␈αassignments␈αof␈αelements
␈↓ ↓H␈↓of␈αthe␈αdomain␈αto␈αthe␈α␈↓↓x␈↓'s.␈α If␈α␈↓↓e␈↓␈αhas␈αfree␈αvariables␈αthat␈αare␈αnot␈αamong␈αthe␈α␈↓↓x␈↓'s,␈αthen␈αthe␈αtruth␈αof␈αthe
␈↓ ↓H␈↓sentence␈α
depends␈α
on␈α
the␈αvalues␈α
assigned␈α
to␈α
these␈αremaining␈α
free␈α
variables.␈α
 ␈↓↓∃x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:e␈↓␈αis␈α
assigned
␈↓ ↓H␈↓true␈αif␈αand␈αonly␈αif␈α␈↓↓e␈↓␈αis␈αassigned␈αtrue␈αfor␈α␈↓↓some␈↓␈αassignment␈αof␈αvalues␈αin␈αthe␈αdomain␈αto␈αthe␈α␈↓↓x␈↓'s.␈α Free
␈↓ ↓H␈↓variables are handled just as before.

␈↓ ↓H␈↓␈↓ α_␈↓↓λx␈↓β1␈↓↓ ... x␈↓βn␈↓↓:u␈↓␈α⊃is␈α⊃assigned␈α⊂a␈α⊃function␈α⊃or␈α⊂predicate␈α⊃according␈α⊃to␈α⊂whether␈α⊃␈↓↓u␈↓␈α⊃is␈α⊂a␈α⊃term␈α⊃or␈α⊂a
␈↓ ↓H␈↓sentence.␈α The␈αvalue␈αof␈α␈↓↓[λx␈↓β1␈↓↓ ... x␈↓βn␈↓↓:u][t␈↓β1␈↓↓,...,t␈↓βn␈↓↓]␈↓␈αis␈αobtained␈αby␈αevaluating␈αthe␈α␈↓↓t␈↓'s␈αand␈αusing␈αthese
␈↓ ↓H␈↓values␈αas␈α
values␈αof␈α
the␈α␈↓↓x␈↓'s␈α
in␈αthe␈α
evaluation␈αof␈α␈↓↓u␈↓.␈α
 If␈α␈↓↓u␈↓␈α
has␈αfree␈α
variables␈αin␈α
addition␈αto␈α
the␈α␈↓↓x␈↓'s,
␈↓ ↓H␈↓the function assigned will depend on them too.

␈↓ ↓H␈↓␈↓ α_Those␈α
who␈αare␈α
familiar␈αwith␈α
the␈α
lambda␈αcalculus␈α
should␈αnote␈α
that␈α
λ␈αis␈α
being␈αused␈α
here␈αin␈α
a
␈↓ ↓H␈↓very␈α
limited␈α
way.␈α Namely,␈α
the␈α
variables␈αin␈α
a␈α
lambda-expression␈α
take␈αonly␈α
elements␈α
of␈αthe␈α
domain
␈↓ ↓H␈↓as␈α⊂values,␈α⊂whereas␈α∂the␈α⊂essence␈α⊂of␈α∂the␈α⊂lambda␈α⊂calculus␈α∂is␈α⊂that␈α⊂they␈α∂take␈α⊂arbitrary␈α⊂functions␈α∂as
␈↓ ↓H␈↓values.  We may call these restricted lambda expressions ␈↓↓first order lambdas␈↓.



␈↓ ↓H␈↓2.  ␈↓αConditional forms.␈↓


␈↓ ↓H␈↓␈↓ α_All the properties we shall use of conditional forms follow from the relation

␈↓ ↓H␈↓␈↓ α_␈↓↓[p ⊃ [␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b] = a] ∧ [¬p ⊃ [␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b] = b]␈↓.

␈↓ ↓H␈↓(If␈α
we␈α
weren't␈α
adhering␈α
to␈α
the␈α
requirement␈α
that␈α
all␈α
terms␈α
be␈α
defined␈α
for␈α
all␈α
values␈α
of␈αthe␈α
variables,
␈↓ ↓H␈↓the situation would be more complicated).

␈↓ ↓H␈↓␈↓ α_It is, however, worthwhile to list separately some properties of conditional forms.

␈↓ ↓H␈↓␈↓ α_First we have the obvious

␈↓ ↓H␈↓␈↓ α_␈↓↓␈↓αif␈↓↓ T ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = a␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α_␈↓↓␈↓αif␈↓↓ F ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = b␈↓.

␈↓ ↓H␈↓␈↓ α_Next we have a ␈↓↓distributive law␈↓ for functions applied to conditional forms, namely

␈↓ ↓H␈↓␈↓ α_␈↓↓f[␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b] = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ f[a] ␈↓αelse␈↓↓ f[b]␈↓.

␈↓ ↓H␈↓This␈α
applies␈αto␈α
predicates␈αas␈α
well␈αas␈α
functions␈αand␈α
can␈α
also␈αbe␈α
used␈αwhen␈α
one␈αof␈α
the␈αarguments␈α
of
␈↓ ↓H␈↓a␈αfunction␈αof␈αseveral␈αarguments␈αis␈αa␈αconditional␈αform.␈α It␈αalso␈αapplies␈αwhen␈αone␈αof␈αthe␈αterms␈αof␈αa
␈↓ ↓H␈↓conditional form is itself a conditional form.
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 94


␈↓ ↓H␈↓Thus

␈↓ ↓H␈↓␈↓ α_␈↓↓␈↓αif␈↓↓ [␈↓αif␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ r] ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ [␈↓αif␈↓↓ q ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b] ␈↓αelse␈↓↓ [␈↓αif␈↓↓ r ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b]␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α_␈↓↓␈↓αif␈↓↓ p ␈↓αthen␈↓↓ [␈↓αif␈↓↓ q ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b] ␈↓αelse␈↓↓ c = ␈↓αif␈↓↓ q ␈↓αthen␈↓↓ [␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ c] ␈↓αelse␈↓↓ [␈↓αif␈↓↓ p ␈↓αthen␈↓↓ b ␈↓αelse␈↓↓ c]␈↓.

␈↓ ↓H␈↓␈↓ α_When␈αthe␈αexpressions␈αfollowing␈α␈↓αthen␈↓␈αand␈α␈↓αelse␈↓␈αare␈αsentences,␈αthen␈αthe␈αconditional␈αform␈αcan
␈↓ ↓H␈↓be replaced by a sentence according to

␈↓ ↓H␈↓␈↓ α_␈↓↓[␈↓αif␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ r] ≡ [p ∧ q] ∨ [¬p ∧ r]␈↓.

␈↓ ↓H␈↓These␈α
two␈α
rules␈α
permit␈αeliminating␈α
conditional␈α
forms␈α
from␈αsentences␈α
by␈α
first␈α
using␈αdistributivity
␈↓ ↓H␈↓to␈αmove␈αthe␈αconditionals␈αto␈αthe␈αoutside␈αof␈αany␈αfunctions␈αand␈αthen␈αreplacing␈αthe␈αconditional␈αform
␈↓ ↓H␈↓by a Boolean expression.

␈↓ ↓H␈↓␈↓ α_Note␈α
that␈α
the␈α
elimination␈α
of␈α
conditional␈α
forms␈αmay␈α
increase␈α
the␈α
size␈α
of␈α
a␈α
sentence,␈αbecause␈α
␈↓↓p␈↓
␈↓ ↓H␈↓occurs␈αtwice␈αin␈αthe␈αright␈αhand␈αside␈αof␈αthe␈αabove␈αequivalence.␈α In␈αthe␈αmost␈αunfavorable␈αcase,␈α␈↓↓p␈↓␈αis
␈↓ ↓H␈↓dominates␈α∩the␈α⊃size␈α∩of␈α⊃the␈α∩expression␈α⊃so␈α∩that␈α⊃writing␈α∩it␈α⊃twice␈α∩almost␈α⊃doubles␈α∩the␈α⊃size␈α∩of␈α⊃the
␈↓ ↓H␈↓expression.

␈↓ ↓H␈↓␈↓ α_Suppose␈αthat␈α␈↓↓a␈↓␈αand␈α␈↓↓b␈↓␈αin␈α␈↓↓␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b␈↓␈αare␈αexpressions␈αthat␈αmay␈αcontain␈αthe␈αsentence␈α␈↓↓p␈↓.
␈↓ ↓H␈↓Occurrences␈α
of␈α
␈↓↓p␈↓␈α
in␈α
␈↓↓a␈↓␈α
can␈αbe␈α
replaced␈α
by␈α
T,␈α
and␈α
occurrences␈α
of␈α␈↓↓p␈↓␈α
in␈α
␈↓↓b␈↓␈α
can␈α
be␈α
replaced␈α
by␈αF.␈α
 This
␈↓ ↓H␈↓follows from the fact that ␈↓↓a␈↓ is only evaluated if ␈↓↓p␈↓ is true and ␈↓↓b␈↓ is evaluated only if ␈↓↓p␈↓ is false.

␈↓ ↓H␈↓␈↓ α_This␈α∂leads␈α⊂to␈α∂a␈α⊂strengthened␈α∂form␈α⊂of␈α∂the␈α⊂law␈α∂of␈α⊂replacement␈α∂of␈α⊂equals␈α∂by␈α⊂equals.␈α∂ The
␈↓ ↓H␈↓ordinary␈α
form␈α
of␈α
the␈α
law␈α
says␈α
that␈α
if␈α
we␈α
have␈α
␈↓↓e = e'␈↓,␈α
then␈α
we␈α
can␈α
replace␈α
any␈α
occurrence␈α
of␈α
␈↓↓e␈↓␈αin␈α
an
␈↓ ↓H␈↓expression␈α⊃by␈α⊃an␈α⊃occurrence␈α⊃of␈α⊃␈↓↓e'␈↓.␈α⊃ However,␈α⊃if␈α⊂we␈α⊃want␈α⊃to␈α⊃replace␈α⊃␈↓↓e␈↓␈α⊃by␈α⊃␈↓↓e'␈↓␈α⊃within␈α⊃␈↓↓a␈↓␈α⊂within
␈↓ ↓H␈↓␈↓αif␈↓␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b␈↓,␈α
then␈α∞we␈α
need␈α
only␈α∞prove␈α
␈↓↓p ⊃ e =e'␈↓,␈α
and␈α∞to␈α
make␈α
the␈α∞replacement␈α
within␈α∞␈↓↓b␈↓␈α
we
␈↓ ↓H␈↓need only prove ␈↓↓¬p ⊃ e = e'␈↓.

␈↓ ↓H␈↓␈↓ α_Additional␈α∀facts␈α∪about␈α∀conditional␈α∀forms␈α∪are␈α∀given␈α∀in␈α∪(McCarthy␈α∀1963a)␈α∀including␈α∪a
␈↓ ↓H␈↓discussion␈αof␈αcanonical␈αforms␈αthat␈αparallels␈α
the␈αcanonical␈αforms␈αof␈αBoolean␈αforms.␈α
 Any␈αquestion
␈↓ ↓H␈↓of␈αequivalence␈αof␈αconditional␈αforms␈αis␈αdecidable␈αby␈αtruth␈αtables␈αanalogously␈αto␈αthe␈αdecidability␈αof
␈↓ ↓H␈↓Boolean forms.



␈↓ ↓H␈↓3.  ␈↓αLambda-expressions.␈↓


␈↓ ↓H␈↓␈↓ α_The␈α∞only␈α∞additional␈α∞rule␈α
required␈α∞for␈α∞handling␈α∞lambda-expressions␈α
in␈α∞first␈α∞order␈α∞logic␈α
is
␈↓ ↓H␈↓called ␈↓↓lambda-conversion␈↓, essentially

␈↓ ↓H␈↓␈↓ α_␈↓↓[λx:e][a] =␈↓ <the result of substituting ␈↓↓e␈↓ for ␈↓↓x␈↓ in ␈↓↓a␈↓>.

␈↓ ↓H␈↓As examples of this rule, we have

␈↓ ↓H␈↓␈↓ α_␈↓↓[λx:␈↓αa␈↓↓ x . y][u . v] = [␈↓αa␈↓↓ [u . v]] . y␈↓.
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 95


␈↓ ↓H␈↓However,␈αa␈α
complication␈αrequires␈α
modifying␈αthe␈α
rule.␈α Namely,␈α
we␈αcan't␈α
substitute␈αfor␈α
a␈αvariable
␈↓ ↓H␈↓and␈α
expression␈αthat␈α
has␈α
a␈αfree␈α
variable␈α
into␈αa␈α
context␈α
in␈αwhich␈α
that␈α
free␈αvariable␈α
is␈αbound.␈α
 Thus
␈↓ ↓H␈↓it␈α∂would␈α∂be␈α∂wrong␈α∂to␈α∂substitute␈α∂␈↓↓x + y␈↓␈α∂for␈α∂␈↓↓x␈↓␈α∂in␈α∂␈↓↓∀y:[x + y = z]␈↓␈α∂or␈α∂into␈α∂the␈α⊂term␈α∂␈↓↓[λy:x + y][u + v]␈↓.
␈↓ ↓H␈↓Before␈α∀doing␈α∀the␈α∪substitution,␈α∀the␈α∀variable␈α∪␈↓↓y␈↓␈α∀would␈α∀have␈α∪to␈α∀be␈α∀replaced␈α∪in␈α∀all␈α∀its␈α∪bound
␈↓ ↓H␈↓occurrences by a fresh variable.

␈↓ ↓H␈↓␈↓ α_Lambda-expressions␈α∀can␈α∀always␈α∃be␈α∀eliminated␈α∀from␈α∃sentences␈α∀and␈α∀terms␈α∃by␈α∀lambda-
␈↓ ↓H␈↓conversion,␈αbut␈αthe␈αexpression␈αmay␈α
increase␈αgreatly␈αin␈αlength␈αif␈α
a␈αlengthy␈αterm␈αreplaces␈αa␈α
variable
␈↓ ↓H␈↓that␈α∞occurs␈α∞more␈α∞than␈α∞once␈α∞in␈α
␈↓↓e␈↓.␈α∞ It␈α∞is␈α∞easy␈α∞to␈α∞make␈α
an␈α∞expression␈α∞of␈α∞length␈α∞␈↓↓n␈↓␈α∞whose␈α∞length␈α
is
␈↓ ↓H␈↓increased to 2␈↓∧n␈↓ by converting its ␈↓↓n␈↓ nested lambda-expressions.



␈↓ ↓H␈↓4.  ␈↓αAlgebraic axioms for S-expressions and lists.␈↓


␈↓ ↓H␈↓␈↓ α_The␈α∂algebraic␈α∞facts␈α∂about␈α∞S-expressions␈α∂are␈α∞expressed␈α∂by␈α∞the␈α∂following␈α∞sentences␈α∂of␈α∞first
␈↓ ↓H␈↓order logic:

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x.(issexp x ⊃ ␈↓αat␈↓↓ x ∨ (issexp ␈↓αa␈↓↓ x ∧ issexp ␈↓αd␈↓↓ x ∧ x = (␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x)))␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x y.(issexp x ∧ issexp y ⊃ issexp(x.y) ∧ ¬␈↓αat␈↓↓(x.y) ∧ x = ␈↓αa␈↓↓(x.y) ∧ y = ␈↓αd␈↓↓(x.y))␈↓.

␈↓ ↓H␈↓Here␈α␈↓↓issexp␈αe␈↓␈αasserts␈αthat␈αthe␈αobject␈α␈↓↓e␈↓␈αis␈αan␈αS-expression␈αso␈αthat␈αthe␈αsentences␈αused␈αin␈αproving␈αa
␈↓ ↓H␈↓particular␈α
program␈αcorrect␈α
can␈αinvolve␈α
other␈αkinds␈α
of␈α
entities␈αas␈α
well.␈α If␈α
we␈αcan␈α
assume␈α
that␈αall
␈↓ ↓H␈↓objects␈αare␈αS-expressions␈αor␈αcan␈αdeclare␈αcertain␈αvariables␈αas␈αranging␈αonly␈αover␈αS-expressions,␈αwe
␈↓ ↓H␈↓can simplify the axioms to

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x.[␈↓αat␈↓↓ x ∨ x = [␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x]]␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x y.[¬␈↓αat␈↓↓[x.y] ∧ x = ␈↓αa␈↓↓[x.y] ∧ y = ␈↓αd␈↓↓[x.y]]␈↓.

␈↓ ↓H␈↓␈↓ α_The algebraic facts about lists are expressed by the following sentences of first order logic:

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x. islist x ⊃ x = ␈↓NIL␈↓↓ ∨ islist ␈↓αd␈↓↓ x␈↓,

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x y. islist y ⊃ islist[x . y]␈↓,

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x y. islist y ⊃ ␈↓αa␈↓↓[x . y] = x ∧ ␈↓αd␈↓↓[x.y] = y␈↓.

␈↓ ↓H␈↓We␈αcan␈α
rarely␈αassume␈α
that␈αeverything␈α
is␈αa␈αlist,␈α
because␈αthe␈α
lists␈αusually␈α
contain␈αatoms␈α
which␈αare
␈↓ ↓H␈↓not themselves lists.

␈↓ ↓H␈↓␈↓ α_These␈α
axioms␈α
are␈α
analogous␈α
to␈α
the␈αalgebraic␈α
part␈α
of␈α
Peano's␈α
axioms␈α
for␈α
the␈αnon-negative
␈↓ ↓H␈↓integers.␈α The␈αanalogy␈αcan␈αbe␈αmade␈αclear␈αif␈αwe␈αwrite␈αPeano's␈αaxioms␈αusing␈α␈↓↓n'␈↓␈αfor␈αthe␈αsuccessor␈αof
␈↓ ↓H␈↓␈↓↓n␈↓ and ␈↓↓n␈↓∧-␈↓ for the predecessor of ␈↓↓n␈↓.  Peano's algebraic axioms then become
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 96


␈↓ ↓H␈↓␈↓ α_␈↓↓∀n: n' ≠ 0␈↓,

␈↓ ↓H␈↓␈↓ α_␈↓↓∀n: (n')␈↓∧-␈↓↓ = n␈↓,

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α_␈↓↓∀n: n ≠ 0 ⊃ (n␈↓∧-␈↓↓)' = n␈↓.

␈↓ ↓H␈↓Integers␈αspecialize␈α lists␈αif␈αwe␈αidentify␈α0␈αwith␈αNIL␈α
and␈αassume␈αthat␈αthere␈αis␈αonly␈αone␈αobject␈α(say␈α
1)
␈↓ ↓H␈↓that can serve as a list element.  Then ␈↓↓n' = cons[1,n]␈↓, and ␈↓↓n␈↓∧-␈↓↓ = ␈↓αd␈↓↓ n␈↓.

␈↓ ↓H␈↓␈↓ α_Clearly␈α∞S-expressions␈α
and␈α∞lists␈α
satisfy␈α∞the␈α∞axioms␈α
given␈α∞for␈α
them,␈α∞but␈α∞unfortunately␈α
these
␈↓ ↓H␈↓algebraic␈α∞axioms␈α∞are␈α∞insufficient␈α∞to␈α∞characterize␈α∂them.␈α∞ For␈α∞example,␈α∞consider␈α∞a␈α∞domain␈α∂of␈α∞one
␈↓ ↓H␈↓element ␈↓↓a␈↓ satisfying

␈↓ ↓H␈↓␈↓ α_␈↓αa␈↓ a = ␈↓αd␈↓ a = a . a = a.

␈↓ ↓H␈↓It␈αsatisfies␈αthe␈αalgebraic␈αaxioms␈αfor␈αS-expressions.␈α We␈αcan␈αexclude␈αit␈αby␈αan␈αaxiom␈α␈↓↓∀x.(␈↓αa␈↓↓␈αx␈α≠␈αx)␈↓,
␈↓ ↓H␈↓but␈αthis␈αwon't␈α
exclude␈αother␈αcircular␈αlist␈α
structures␈αthat␈αeventually␈αreturn␈α
to␈αthe␈αsame␈α
element␈αby
␈↓ ↓H␈↓some␈α∂␈↓αa-d␈↓␈α∂chain.␈α∂ Actually␈α∞we␈α∂want␈α∂to␈α∂exclude␈α∂all␈α∞infinite␈α∂chains,␈α∂because␈α∂most␈α∂LISP␈α∞programs
␈↓ ↓H␈↓won't␈αterminate␈αunless␈αevery␈α␈↓αa-d␈↓␈αchain␈αeventually␈αterminates␈αin␈αan␈αatom.␈α This␈αcannot␈αbe␈αdone␈αby
␈↓ ↓H␈↓any finite set of axioms.



␈↓ ↓H␈↓5.  ␈↓αAxiom schemas of induction.␈↓


␈↓ ↓H␈↓␈↓ α_In␈αorder␈αto␈α
exclude␈αinfinite␈αlist␈αstructures␈α
we␈αneed␈αaxiom␈α
schemas␈αof␈αinduction␈αanalogous␈α
to
␈↓ ↓H␈↓Peano's for the integers.  Peano's induction schema is ordinarily written

␈↓ ↓H␈↓␈↓ α_␈↓↓P(0) ∧ ∀n:(P(n) ⊃ P(n')) ⊃ ∀n:P(n)␈↓.

␈↓ ↓H␈↓Here␈α␈↓↓P(n)␈↓␈αis␈αan␈αarbitrary␈α
predicate␈αof␈αintegers,␈αand␈αwe␈α
get␈αparticular␈αinstances␈αof␈αthe␈α
schema␈αby
␈↓ ↓H␈↓substituting␈αparticular␈αpredicates.␈α It␈αis␈αcalled␈αan␈αaxiom␈αschema␈αrather␈αthan␈αan␈αaxiom,␈αbecause␈αwe
␈↓ ↓H␈↓consider␈α∂the␈α∂schema,␈α∂which␈α∂is␈α∂not␈α∂properly␈α⊂a␈α∂sentence␈α∂of␈α∂first␈α∂order␈α∂logic,␈α∂as␈α∂standing␈α⊂for␈α∂the
␈↓ ↓H␈↓infinite collection of axioms that arise from it by substituting all possible predicates for ␈↓↓P␈↓.

␈↓ ↓H␈↓Peano's induction schema can also be written

␈↓ ↓H␈↓␈↓ α_␈↓↓∀n:(n = 0 ∨ P(n␈↓∧-␈↓↓) ⊃ P(n)) ⊃ ∀n:P(n)␈↓,

␈↓ ↓H␈↓and the equivalence of the two forms is easily proved.

␈↓ ↓H␈↓␈↓ α_The S-expression analog is

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x:[issexp x ⊃ [␈↓αat␈↓↓ x ∨ P[␈↓αa␈↓↓ x] ∧ P[␈↓αd␈↓↓ x] ⊃ P[x]]] ⊃ ∀x:[issexp x ⊃ P[x]]␈↓,

␈↓ ↓H␈↓or, assuming everything is an S-expression
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 97


␈↓ ↓H␈↓␈↓ α_␈↓↓∀x:[␈↓αat␈↓↓ x ∨ P[␈↓αa␈↓↓ x] ∧ P[␈↓αd␈↓↓ x] ⊃ P[x]] ⊃ ∀x:P[x]␈↓.

␈↓ ↓H␈↓␈↓ α_The corresponding axiom schema for lists is

␈↓ ↓H␈↓␈↓ α_␈↓↓∀u:[islist u ⊃ [␈↓αn␈↓↓ u ∨ P[␈↓αd␈↓↓ u] ⊃ P[u]]] ⊃ ∀u:[islist u ⊃ P[u]]␈↓.

␈↓ ↓H␈↓␈↓ α_These␈α∂schemas␈α∞are␈α∂called␈α∞principles␈α∂of␈α∞␈↓↓structural␈α∂induction␈↓,␈α∞since␈α∂the␈α∞induction␈α∂is␈α∂on␈α∞the
␈↓ ↓H␈↓structure of the entities involved.

␈↓ ↓H␈↓␈↓ α_Even␈αthe␈αaxiom␈αschemas␈αdon't␈αassure␈αus␈αthat␈αthe␈αonly␈αdomain␈αsatisfying␈αthe␈αaxioms␈αis␈αthat
␈↓ ↓H␈↓of␈αthe␈αintegers␈αor␈αthe␈αS-expressions␈αas␈αthe␈α
case␈αmay␈αbe.␈α Any␈αfirst␈αorder␈αtheory␈αwhose␈αaxioms␈α
can
␈↓ ↓H␈↓be␈α
given␈αeffectively␈α
admits␈α
the␈αso-called␈α
␈↓↓non-standard␈αmodels␈↓.␈α
 However,␈α
it␈αseems␈α
likely␈α
that␈αthe
␈↓ ↓H␈↓non-standard␈α
models␈α
of␈α
S-expressions,␈α
like␈α
the␈α
non-standard␈α
models␈α
of␈α
integers,␈α
will␈α
agree␈αwith
␈↓ ↓H␈↓the standard model except for all sentences of practical interest.



␈↓ ↓H␈↓6.  ␈↓αProofs by structural induction.␈↓


␈↓ ↓H␈↓␈↓ α_Recall that the operation of appending two lists is defined by

␈↓ ↓H␈↓1)␈↓ α8 ␈↓↓u * v ← ␈↓αif␈↓↓ n u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓.

␈↓ ↓H␈↓Let␈α∩us␈α⊃assume␈α∩that␈α∩␈↓↓u␈α⊃*␈α∩v␈↓␈α⊃is␈α∩defined␈α∩for␈α⊃all␈α∩␈↓↓u␈↓␈α⊃and␈α∩␈↓↓v␈↓,␈α∩i.e.␈α⊃the␈α∩computation␈α∩described␈α⊃above
␈↓ ↓H␈↓terminates␈α
for␈α
all␈α
␈↓↓u␈↓␈α
and␈α
␈↓↓v␈↓;␈α
we␈α
will␈α
show␈α∞how␈α
to␈α
prove␈α
it␈α
later.␈α
 Then␈α
we␈α
can␈α
replace␈α
(1)␈α∞by␈α
the
␈↓ ↓H␈↓sentence

␈↓ ↓H␈↓2)␈↓ α8 ␈↓↓∀u v:[islist u ∧ islist v ⊃ [u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]]]␈↓.

␈↓ ↓H␈↓Now␈α⊂suppose␈α⊃we␈α⊂would␈α⊃like␈α⊂to␈α⊃prove␈α⊂␈↓↓∀v:[␈↓NIL␈↓↓␈α⊃*␈α⊂v␈α⊂=␈α⊃v]␈↓.␈α⊂ This␈α⊃is␈α⊂quite␈α⊃trivial;␈α⊂we␈α⊃need␈α⊂only
␈↓ ↓H␈↓substitute NIL for ␈↓↓x␈↓ in (2), getting

␈↓ ↓H␈↓→␈↓↓␈↓NIL␈↓↓ * v ␈↓ β( = ␈↓αif␈↓↓ n ␈↓NIL␈↓↓ ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ a ␈↓NIL␈↓↓ . [␈↓αd␈↓↓ ␈↓NIL␈↓↓ * v]

␈↓ ↓H␈↓↓␈↓ β( = v␈↓.

␈↓ ↓H␈↓Next␈αconsider␈αproving␈α␈↓↓∀u:[u␈α*␈α␈↓NIL␈↓↓␈α=␈αu]␈↓.␈α This␈αcannot␈αbe␈αdone␈αby␈αsimple␈αsubstitution,␈αbut␈αit␈αcan
␈↓ ↓H␈↓be done as follows:  First substitute ␈↓↓λu:[u * ␈↓NIL␈↓↓ = u]␈↓ for ␈↓↓P␈↓ in the induction schema

␈↓ ↓H␈↓␈↓ α_␈↓↓∀u:[islist u ⊃ [␈↓αn␈↓↓ u ∨ P[␈↓αd␈↓↓ u] ⊃ P[u]]] ⊃ ∀u:[islist u ⊃ P[u]]␈↓,

␈↓ ↓H␈↓getting

␈↓ ↓H␈↓␈↓ α_␈↓↓∀u:[islist␈αu␈α⊃␈α[␈↓αn␈↓↓␈αu␈α∨␈α[λu:␈αu␈α
*␈α␈↓NIL␈↓↓␈α=␈αu][␈↓αd␈↓↓␈αu]␈α⊃␈αλu:[u␈α*␈α
␈↓NIL␈↓↓␈α=␈αu][u]]]␈α⊃␈α∀u:[islist␈αu␈α⊃␈αλu:[u␈α
*
␈↓ ↓H␈↓↓␈↓NIL␈↓↓ = u][u]]␈↓.

␈↓ ↓H␈↓Carrying out the indicated lambda conversions makes this

␈↓ ↓H␈↓3)␈↓ α8 ␈↓↓∀u:[islist u ⊃ [␈↓αn␈↓↓ u ∨ ␈↓αd␈↓↓ u * ␈↓NIL␈↓↓ = ␈↓αd␈↓↓ u] ⊃ u * ␈↓NIL␈↓↓ = u] ⊃ ∀u:[islist u ⊃ u * ␈↓NIL␈↓↓ = u]␈↓.
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 98


␈↓ ↓H␈↓␈↓ α_Next␈α
we␈α
must␈α
use␈α
the␈α
recursive␈α
definition␈α
of␈α
␈↓↓u*v␈↓.␈α
 There␈α
are␈α
two␈α
cases␈α
according␈αto␈α
whether
␈↓ ↓H␈↓␈↓αn␈↓␈α␈↓↓u␈↓␈αor␈αnot.␈α In␈αthe␈αfirst␈αcase,␈αwe␈αsubstitute␈αNIL␈αfor␈α␈↓↓v␈↓␈αand␈αget␈αNIL*NIL = NIL,␈αand␈αin␈αthe␈αsecond
␈↓ ↓H␈↓case␈α
we␈α
use␈α
the␈α
hypothesis␈α
␈↓αd␈↓ u * NIL = ␈↓αd␈↓ u␈α
and␈α∞the␈α
third␈α
algebraic␈α
axiom␈α
for␈α
lists␈α
to␈α∞make␈α
the
␈↓ ↓H␈↓simplification

␈↓ ↓H␈↓4)␈↓ α8 ␈↓↓␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * ␈↓NIL␈↓↓] = ␈↓αa␈↓↓ u . ␈↓αd␈↓↓ u = u.␈↓

␈↓ ↓H␈↓Combining␈α
the␈α
cases␈α
gives␈α
the␈α
hypothesis␈α
of␈α(3)␈α
and␈α
hence␈α
its␈α
conclusion,␈α
which␈α
is␈α
the␈αstatement␈α
to
␈↓ ↓H␈↓be proved.



␈↓ ↓H␈↓7.  ␈↓αFirst Order Theory of Partial Functions␈↓


␈↓ ↓H␈↓␈↓ α_In␈αthe␈αprevious␈α
section␈αwe␈αproved␈α
facts␈αabout␈αLisp␈α
functions␈αstarting␈αfrom␈α
the␈αassumption
␈↓ ↓H␈↓that␈α
their␈α
computation␈α
terminates␈α
for␈α
all␈α
values␈α
of␈α
the␈α
arguments.␈α
 This␈α
enabled␈α
us␈α
to␈α
write␈α
the
␈↓ ↓H␈↓definition␈α
as␈α
a␈αsentence␈α
of␈α
first␈α
order␈αlogic.␈α
 However,␈α
we␈α
often␈αmust␈α
deal␈α
with␈α
partial␈αfunctions
␈↓ ↓H␈↓that␈α
don't␈αterminate␈α
for␈α
all␈αarguments.␈α
 Sometimes␈α
the␈αproblem␈α
is␈α
to␈αprove␈α
that␈α
the␈αcomputation
␈↓ ↓H␈↓terminates, and sometimes the problem is to prove that it doesn't.

␈↓ ↓H␈↓␈↓ α_Even␈αthough␈αa␈αrecursively␈αdefined␈αfunction␈αis␈αnot␈αknown␈αto␈αterminate,␈αit␈αis␈αstill␈αpossible␈αto
␈↓ ↓H␈↓characterize␈α
it␈αby␈α
a␈α
sentence␈αof␈α
first␈αorder␈α
logic␈α
and␈αby␈α
a␈αspecial␈α
axiom␈α
schema␈αof␈α
first␈αorder␈α
logic.
␈↓ ↓H␈↓This is done as follows:

␈↓ ↓H␈↓␈↓ α_Consider␈α∪the␈α∪domain␈α∪␈↓↓SE␈↓␈α∀of␈α∪S-expressions␈α∪to␈α∪be␈α∀imbedded␈α∪in␈α∪a␈α∪larger␈α∀domain.␈α∪ For
␈↓ ↓H␈↓concreteness␈αwe␈αmay␈αsuppose␈α
that␈αthis␈αdomain␈αhas␈αonly␈α
one␈αelement␈α␈↓εW␈↓␈αbesides␈α
the␈αS-expressions
␈↓ ↓H␈↓that␈αwe␈αwill␈αtake␈αas␈αthe␈αvalue␈αof␈αa␈αfunction␈αwhenever␈αits␈αcomputation␈αfails␈αto␈αterminate.␈α We␈αmay
␈↓ ↓H␈↓further␈α∞assume␈α∞that␈α∞the␈α
basic␈α∞Lisp␈α∞functions␈α∞take␈α
␈↓πW␈↓␈α∞as␈α∞value␈α∞whenever␈α
an␈α∞argument␈α∞has␈α∞value␈α
␈↓πW␈↓.
␈↓ ↓H␈↓However,␈αneither␈αassumption␈αwill␈αever␈αbe␈αused␈αin␈αa␈αproof,␈αso␈αtheir␈αneed␈αbe␈αno␈αaxioms␈αexpressing
␈↓ ↓H␈↓them.

␈↓ ↓H␈↓␈↓ α_Recursive␈αdefinitions␈α
give␈αrise␈α
to␈αlogical␈α
sentences␈αjust␈α
as␈αbefore␈α
so␈αthat␈α
␈↓↓append␈↓␈αis␈α
described
␈↓ ↓H␈↓by

␈↓ ↓H␈↓5)␈↓ α8  ␈↓↓∀u v.[u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]]␈↓,

␈↓ ↓H␈↓but now it is not assumed that ␈↓↓u * v␈↓ is necessarily a list; this must be proved as follows:

␈↓ ↓H␈↓␈↓ α_We take

␈↓ ↓H␈↓6)␈↓ α8  ␈↓↓P(u) = islist[u * v]␈↓

␈↓ ↓H␈↓in the axioms schema of list induction getting

␈↓ ↓H␈↓7)␈↓ α8  ␈↓↓islist[␈↓NIL␈↓↓ * v] ∧ ∀u.[¬␈↓αn␈↓↓ u ∧ islist[␈↓αd␈↓↓ u * v] ⊃ islist[u * v]]⊃ ∀u.islist[u * v]␈↓.

␈↓ ↓H␈↓Now␈αthe␈αpremisses␈αof␈α(7)␈αare␈αeasily␈αproved␈αfrom␈α(5)␈αand␈α
the␈αfact␈αthat␈αif␈α␈↓↓u␈↓␈αis␈αa␈αlist,␈αso␈αis␈α␈↓↓x . u␈↓.␈α
 As
␈↓ ↓H␈↓we␈α⊂shall␈α⊂see,␈α⊂the␈α⊂resulting␈α⊂proof␈α⊂that␈α⊂the␈α⊂computation␈α⊂of␈α⊂␈↓↓u * v␈↓␈α⊂is␈α⊂a␈α⊂list␈α⊂can␈α⊂be␈α⊂taken␈α⊂as␈α∂also
␈↓ ↓H␈↓proving that the computation terminates.